This application is based on and hereby claims priority to German Patent Application No. 198 14 109.2 filed on Mar. 30, 1998, the contents of which are hereby incorporated by reference.
The invention is directed to a method for comparing electrical circuits to one another.
In the design of a digital circuit, the quality assurance before the start of production requires 30% to 70% of the entire development time. During the quality assurance, attempts to find faults in the circuit are made by intensive simulation. Even after the end of the simulation, only a part of the behavior of a digital circuit has been investigated, so that it must always be considered that faulty designs can go into production. An inconsistency in an electrical circuit noticed after the beginning of production and a correction following thereupon require time-consuming and expensive refitting work.
The quality assurance is intended to assure that description forms of different phase of the circuit design for a circuit exhibit identical input/output behavior. It is thereby customary to represent (digital) circuits as finite automatons with Boolean input/output and truth values. Prof. Dr. Hans-Jochen Schneider (Editor), xe2x80x9cLexikon der Informatik und Datenverarbeitungxe2x80x9d, R. Oldenbourg Verlag Munich, 1986, ISBN 3-486-22662-2, pp. 51-54. When description forms of different phases of the circuit design are compared to one another, then the circuits underlying the description forms are thereby compared.
In the framework of generating models, circuits that derive from the respective design steps are imaged onto finite automatons. A determination regarding the extent to which inputs and outputs of the automatons are to be allocated to one another follows (input/output matching). Whether identical input values also lead to identical outputs in the automatons is examined in view of this allocation. When this is not the case, a diagnosis is produced that allows the user to analyze the fault.
T. Filkorn, Symbolische Methoden fxc3xcr die Verifikation endlicher Zustandssysteme, Dissertation, Institut fxc3xcr Informatik at the Technical University, Munich, 1992, pp. 82-97. discloses a method with the object of simplifying a product machine, i.e. a combination of two automatons. The set of all status transition functions is thereby investigated and resolved into sub-sets of functions that behave identically on the set of obtainable statusses. Given automatons similar to one another, these sub-sets contain an equal number of functions from both automatons and are even often two-element, so that the allocation of the operands proceeds therefrom. One disadvantage of this method is comprised therein that differences between the two automatons do not lead to a usable result. When two status transition functions that logically belong together differ, then a correct allocation does not occur.
What is understood by status coding is a representation of a circuit in the form of an automaton, whereby this automaton comprises statusses and status transition functions.
A structural comparison of two circuits is a matter of a comparison of the combinatorial logic representing the circuit, given the assumption that the status codings of both circuits have occured in the same way.
In a sequential comparison, identical input/output behavior of two circuits is verified, whereby the respective circuits can exhibit different status.
Structurally identical automatons exhibit the same status; structurally similar automatons exhibit nearly identical status.
What is understood below by a resolution is a set that is composed of disjunctive sets. A group is an element of a resolution, whereby this element again represents a set. A sub-resolution is a sub-set of a resolution. A refinement (of a resolution) derives from the wording as a xe2x80x9cfinerxe2x80x9d subdivision of the resolution. The relationship that has been presented is explained on the basis of a brief example:
An of the invention is to create a method for comparing electrical circuits, to thus not have to completely cover the design process, and, given different but structurally automatons, to assure an efficient comparison on the basis of an abstraction of status transition functions of the automatons, which describe the electrical circuits.
The circuits to be compared can proceed from different description forms for the design of an electrical circuit. It is to be assured that the electrical circuits corresponding to the different description forms are identical. Each description form represents a separate electrical circuit.
According to the method of the invention for comparison of electrical circuits, a representation of a first circuit is provided by a first automaton. A representation of a second circuit is provided by a second automaton. An allocation of input variables of the first automaton onto input variables of the second automaton and an allocation of output variables of the first automaton onto output variables of the second automaton is provided. A base set is provided with operands of the first and of the second automaton. Preceding from a predetermined resolution of the base set, implementing the following steps:
1) determining which data dependency exists between operands, input variables and output variables for each operand of the resolution, wherein
determining those operands and those input variables on which a status transition function of the operand is dependent, and
determining those operands and those output variables that are dependent on the operand for each operand;
2) combining those operands that are determined by identical data dependencies according to step 1) in a group of the resolution; and
3) implementing step 2) for all operands, so that a refinement of the resolution is determined.
Operands of the respective group are considered allocated to one another. A comparison of the two circuits underlying the automatons is implemented on the basis of the identified allocations.
A method for the comparison of electrical circuits is created wherein a first circuit is represented by a first automaton and a second circuit is represented by a second automaton. Input variables and output variables of the first automaton are imaged onto corresponding input variables and output variables of the second automaton. A basic set comprises operands of the first and of the second automaton. Proceeding from a resolution of the basic set, the following steps are implemented:
(1) For each operand of the resolution, a determination is made as to which dependencies exist between operands, input variables and output variables, whereby operands from a group can be distinguished from one another;
(2) those operands that are defined by identical data dependencies according to step (1) are combined in a group of the resolution and;
(3) step (2) is implemented for all operands, so that a refinement of the resolution is determined.
Operands of a group of the refinement are allocated to one another and a comparison of the electrical circuits underlying the automatons is implemented on the basis of the identified allocation.
One step for the comparison of two circuits that are respectively represented by a finite automaton to one another is comprised in the paired allocation of a respective operand of both automatons to one another, as a result whereof what status transition functions are to be compared and what operands are to be identified in the comparison (structural comparison) are determined.
A sequential comparison requires a predetermined variable ordering, i.e. a sequence, in which operands are noted and processed, whereby this sequence substantially determines the expense of the sequential comparison. When the variable ordering is determined with the inventive method, then a drastic reduction of the run time of the sequential comparison or a clearly reduced demand for memory capacity to be made available results.
In a development of the invention, an iteration of the method is implemented such that the refinement of the resolution is inserted as a new resolution and one continues with step (1) until no farther-reaching refinement of the resolution is determined by a next iteration.
Advantageously, an identical number of operands of the first and of the second automaton are present in a group. The group is called balanced in this case. A matching group is a two-element balanced group. When a plurality of matching groups are obtained at the end of the preferably iterative application of the method, then an unambiguous allocation of the operands contained in the respective matching group results therefrom.
In another development, a refinement of the resolution is achieved with at least one of the following possibilities:
a) In a support method, those operands and those input variables on which the status transition function of the operand x depends are determined for each operand x;
b) in an inverse support method, those operands and those output variables that are dependent on the operand are determined for each operand.
Let it be thereby noted that the basic set preferably covers all operands of both automatons. The dependency on the other operands of an automaton is determined for each operand x for the respective automaton. A possible presentation occurs on the basis of a data dependency graph. The data dependency graph comprises a node for each operand of the respective automaton and an arrow from a node u to a node v when node u lies in the support of node v. Conversely, then node v then lies in the inverse support of the node u.
Another development of the invention is that refinements are additionally generated on the basis of a simulation method in that, on the basis of value occupancies of the input variables and of the operands that are preferably randomly generated, identical value occupancies of the status transition functions underlying the operands are determined.
Another development of the invention is comprised in correcting an incorrectly determined refinement of the resolution on the basis of a coarsening method, in that groups with a respectively different number of operands of the first automaton and of the second automaton are combined in a group.
In general, unbalanced groups of the resolution wherein an allocation of operands of the two automatons to be compared cannot occur are counteracted by the coarsening method.
In the framework of an additional development of the invention, the two automatons are sequentially compared to one another. Precisely given such a sequential comparison, it is advantageous when the automatons to be compared are structurally similar. A sequential comparison occurs in that the first and the second automaton are operated with one another to form a product automaton. An input signal is applied both to the first as well as to the second automaton, and the resulting output signals of the first and of the second automaton are compared to one another. Preferably, such a comparison is implemented with an exclusive-OR operation that indicates with a output value xe2x80x9c0xe2x80x9d (or, respectively, xe2x80x9cFALSExe2x80x9d) that the output signals of the two automatons are different.
Binary decision diagrams (BDDs) are preferably utilized in the sequential comparison (also see R. Bryant, Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. on Computers, Vol.C-35, No. 8, August 1996, pp. 677-691.). A variable ordering within the BDDs determines the sequence in which the variables are proposed. How much memory the BDDs use and the time in which they can be processed are prescribed to a substantial extent by the variable ordering.
The method of the invention can be utilized for determining the variable ordering. Thus, the variable ordering is determined according to the identified allocations of the operands in that operands allocated to one another are arranged behind one another.
Exemplary embodiments of the invention are presented in greater detail on the basis of the following Figures.